module Wnioskowanie (wywnioskuj) where

import Drzewo
import qualified Zjednanie
import Data.Char

weźTyp :: OpisaneWyrażenie -> Typ
weźTyp (OZmienna _ a) = a
weźTyp (OFunkcja _ _ a) = a
weźTyp (OWywołanie _ _ a) = a


-- opisz/oznacz
opisz :: Wyrażenie -> OpisaneWyrażenie
opisz w = let (a,_,_) = (_opisz [] []  'a' w) in a

_opisz ::  [(Nazwa, Typ)] -> [(Nazwa, Typ)] -> Char -> Wyrażenie -> (OpisaneWyrażenie, Char, [(Nazwa, Typ)])
_opisz tabela związane c (Zmienna x) =
  case lookup x związane of
     Just a -> (OZmienna x a, c, tabela)
     Nothing -> case lookup x tabela of
         Just a ->  (OZmienna x a, c, tabela)
         Nothing -> let n =  następny c in (OZmienna x (TZmiennej [c]), n, (x, (TZmiennej [c])):tabela)
_opisz  tabela związane c (Funkcja x e) =
  let n = następny c -- nowy typ dla x
      (ow, nn, tt) = _opisz tabela ((x,(TZmiennej [c])):związane) n e in
      (OFunkcja x ow (Strzałka (TZmiennej [c]) (weźTyp ow)), nn, tt)
_opisz tabela związane c (Wywołanie w1 w2) =
  let n = następny c
      (xd1, nn, tt) = _opisz tabela związane n w1
      (xd2, nnn, ttt) = _opisz tt związane nn w2
  in
    (OWywołanie xd1 xd2 (TZmiennej [c]), nnn, ttt)
    
    
następny :: Char -> Char
--następny 'z' = 'Q' -- :(
następny x = chr (ord x + 1)


-- zbiera ograniczenia dla zjednywania
zbierz :: [OpisaneWyrażenie] -> [(Typ, Typ)] -> [(Typ, Typ)]
zbierz [] u = u
zbierz ((OZmienna _ _) : r) u = zbierz r u
zbierz ((OFunkcja _ ow _) : r) u = zbierz (ow : r) u
zbierz ((OWywołanie ow1 ow2 a) : r) u =
  let (f, b) = (weźTyp ow1, weźTyp ow2) in
    zbierz (ow1 : ow2 : r) ((f, Strzałka b a) : u)
       
wywnioskuj :: Wyrażenie -> Maybe Typ
wywnioskuj wyrażenie =
  let ow = opisz wyrażenie
      zb = zbierz [ow] [] in
      (\z -> Zjednanie.dawaj z (weźTyp ow)) <$> Zjednanie.zjednaj zb
    
